crng{i:l}  Type{i'} 

latex

Definitions	crng{i:l}, t  T, prop{i:l}, x:A. B(x), rng{i:l}
Lemmas	rng times wf, rng car wf, comm wf, rng wf